Skip to content

feat(RepresentationTheory/Homological/ContCohomology): add inflation maps in continuous cohomology#41545

Open
rmhi wants to merge 10 commits into
leanprover-community:masterfrom
rmhi:rh_inflation
Open

feat(RepresentationTheory/Homological/ContCohomology): add inflation maps in continuous cohomology#41545
rmhi wants to merge 10 commits into
leanprover-community:masterfrom
rmhi:rh_inflation

Conversation

@rmhi

@rmhi rmhi commented Jul 9, 2026

Copy link
Copy Markdown
Collaborator

For a normal subgroup N of a topological group G, define the inflation maps
from H^n(G/N, \pi^N) to H^n(G, \pi), where H^n is the n-th continuous cohomology.
These maps are defined as a natural transformation.

Open in Gitpod

@github-actions

github-actions Bot commented Jul 9, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 888020e604

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
10 files Mathlib.Topology.Algebra.Group.ClosedSubgroup Mathlib.Topology.Algebra.Group.Extension Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete Mathlib.Topology.Algebra.ProperAction.AddTorsor Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.ProperAction.Torsor Mathlib.Topology.Covering.Quotient Mathlib.Topology.Maps.Strict.Basic
 1
Mathlib.RepresentationTheory.Homological.ContCohomology.Inflation (new file) 1918

Declarations diff (regex)

+ ResMap_eq
+ ResMap_id_left
+ ResMap_id_right
+ _root_.QuotientTopGroup.coe_mk
+ _root_.QuotientTopGroup.mk
+ _root_.TopRep.resolutionXRes
+ _root_.continuousCohomologyFunctor
+ cochainsResMap
+ cochainsResMap_comp
+ cochainsResMap_eq
+ cochainsResMap_f_eq
+ cochainsResMap_id
+ cochainsResMap_id_left
+ cochainsResMap_id_right
+ cocyclesResMap
+ cocyclesResMap_comp
+ cocyclesResMap_id
+ coind₁Res_id
+ comp_id
+ continuousCohomologyFunctor_obj
+ homogeneousCochainsFunctor
+ homogeneousCochainsFunctor_obj
+ homogeneousCochainsResNatTrans
+ homogeneousCochainsResNatTrans_app_f
+ homogeneousCochainsXRes
+ homogeneousCochainsXRes_succ
+ homogeneousCochainsXRes_zero
+ id_comp
+ inflApp
+ inflApp_naturality
+ inflApp_naturality_aux
+ inflNatTrans
+ inflι
+ inflιapp
+ inflιapp_apply
+ instance {H : Type*} [Monoid H] (φ : H →* G) : (resFunctor (k := k) φ).Additive
+ invariantsRes
+ invariantsResMap_eq
+ invariantsResMap_id
+ invariantsResNatTrans
+ le_relInvariantsRho_ker
+ ofHom_comp
+ relInvariants
+ relInvariantsFunctor
+ relInvariantsInfl
+ relInvariantsIntertwining
+ relInvariantsIntertwining'
+ relInvariantsRho
+ resMap
+ resMap_comp
+ resMap_id
+ resNatTrans
+ resNatTrans_app
+ resolution'Functor
+ resolution'Res
+ resolution'ResNatTrans
+ resolutionResMap
+ resolutionResMap_comp
+ resolutionResMap_comp_d
+ resolutionResMap_eq
+ resolutionResMap_id
+ resolutionResMap_id_fst
+ resolutionResMap_id_snd
+ resolutionResMap_succ
+ resolutionResMap_zero
+ resolutionXRes_comp
+ resolutionXRes_comp_d
+ resolutionXRes_id
+ resolutionXRes_naturality
+ resolutionXRes_succ
+ resolutionXRes_zero
+ rho_mem_relInvariants
+ π_resMap
- cochainsMap
- cochainsMap_comp
- cochainsMap_id
- cocyclesMap
- cocyclesMap_comp
- cocyclesMap_id
- map
- map_comp
- map_id
- π_map

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 888020e).

  • +94 new declarations
  • −16 removed declarations
+ContIntertwiningMap.comp_id
+ContIntertwiningMap.id_comp
+ContRepresentation.coind₁Res_id
+ContRepresentation.le_relInvariantsRho_ker
+ContRepresentation.relInvariants
+ContRepresentation.relInvariantsInfl
+ContRepresentation.relInvariantsIntertwining
+ContRepresentation.relInvariantsIntertwining'
+ContRepresentation.relInvariantsRho
+ContRepresentation.relInvariantsRho.congr_simp
+ContRepresentation.relInvariantsRho_toMonoidHom_apply
+ContRepresentation.rho_mem_relInvariants
+ContinuousCohomology.ResMap_eq
+ContinuousCohomology.ResMap_eq_assoc
+ContinuousCohomology.ResMap_id_left
+ContinuousCohomology.ResMap_id_right
-ContinuousCohomology.cochainsMap
-ContinuousCohomology.cochainsMap_comp
-ContinuousCohomology.cochainsMap_comp_assoc
-ContinuousCohomology.cochainsMap_f
-ContinuousCohomology.cochainsMap_f_hom
-ContinuousCohomology.cochainsMap_id
+ContinuousCohomology.cochainsResMap
+ContinuousCohomology.cochainsResMap_comp
+ContinuousCohomology.cochainsResMap_comp_assoc
+ContinuousCohomology.cochainsResMap_eq
+ContinuousCohomology.cochainsResMap_eq_assoc
+ContinuousCohomology.cochainsResMap_f
+ContinuousCohomology.cochainsResMap_f_eq
+ContinuousCohomology.cochainsResMap_f_eq_assoc
+ContinuousCohomology.cochainsResMap_f_hom
+ContinuousCohomology.cochainsResMap_id
+ContinuousCohomology.cochainsResMap_id_left
+ContinuousCohomology.cochainsResMap_id_right
-ContinuousCohomology.cocyclesMap
-ContinuousCohomology.cocyclesMap_comp
-ContinuousCohomology.cocyclesMap_comp_assoc
-ContinuousCohomology.cocyclesMap_id
+ContinuousCohomology.cocyclesResMap
+ContinuousCohomology.cocyclesResMap_comp
+ContinuousCohomology.cocyclesResMap_comp_assoc
+ContinuousCohomology.cocyclesResMap_id
+ContinuousCohomology.continuousCohomologyFunctor_obj
+ContinuousCohomology.homogeneousCochainsFunctor
+ContinuousCohomology.homogeneousCochainsFunctor_obj
+ContinuousCohomology.homogeneousCochainsResNatTrans
+ContinuousCohomology.homogeneousCochainsResNatTrans_app_f
+ContinuousCohomology.homogeneousCochainsXRes
+ContinuousCohomology.homogeneousCochainsXRes_succ
+ContinuousCohomology.homogeneousCochainsXRes_zero
+ContinuousCohomology.inflApp
+ContinuousCohomology.inflApp_naturality
+ContinuousCohomology.inflNatTrans
-ContinuousCohomology.map
-ContinuousCohomology.map_comp
-ContinuousCohomology.map_comp_assoc
-ContinuousCohomology.map_id
+ContinuousCohomology.resMap
+ContinuousCohomology.resMap_comp
+ContinuousCohomology.resMap_comp_assoc
+ContinuousCohomology.resMap_id
+ContinuousCohomology.resNatTrans
+ContinuousCohomology.resNatTrans_app
+ContinuousCohomology.resolution'Functor
+ContinuousCohomology.resolution'Functor_map_f
+ContinuousCohomology.resolution'Functor_obj_X_V
+ContinuousCohomology.resolution'Functor_obj_X_hV3
+ContinuousCohomology.resolution'Functor_obj_X_ρ
+ContinuousCohomology.resolution'Functor_obj_d
+ContinuousCohomology.resolution'Res
+ContinuousCohomology.resolution'ResNatTrans
+ContinuousCohomology.resolutionResMap
+ContinuousCohomology.resolutionResMap_comp
+ContinuousCohomology.resolutionResMap_comp_d
+ContinuousCohomology.resolutionResMap_eq
+ContinuousCohomology.resolutionResMap_eq_assoc
+ContinuousCohomology.resolutionResMap_id
+ContinuousCohomology.resolutionResMap_id_fst
+ContinuousCohomology.resolutionResMap_id_snd
+ContinuousCohomology.resolutionResMap_succ
+ContinuousCohomology.resolutionResMap_zero
+ContinuousCohomology.resolutionXRes_comp
+ContinuousCohomology.resolutionXRes_comp_d
+ContinuousCohomology.resolutionXRes_id
+ContinuousCohomology.resolutionXRes_naturality
+ContinuousCohomology.resolutionXRes_succ
+ContinuousCohomology.resolutionXRes_zero
+ContinuousCohomology.termHₜ
+ContinuousCohomology.termHₜFunct
-ContinuousCohomology.π_map
-ContinuousCohomology.π_map_assoc
+ContinuousCohomology.π_resMap
+ContinuousCohomology.π_resMap_assoc
+ContinuousLinearMap.restrict.congr_simp
+QuotientTopAddGroup.coe_mk
+QuotientTopAddGroup.mk
+QuotientTopGroup.coe_mk
+QuotientTopGroup.mk
+TopRep.inflι
+TopRep.inflιapp
+TopRep.inflιapp_apply
+TopRep.instAdditiveResFunctor
+TopRep.invariantsRes
+TopRep.invariantsResMap_eq
+TopRep.invariantsResMap_id
+TopRep.invariantsResNatTrans
+TopRep.ofHom_comp
+TopRep.relInvariantsFunctor
+TopRep.resolutionXRes
+continuousCohomologyFunctor

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type (weak)
5005 1 exposed public sections

Current commit 888020e604
Reference commit 2d00c9242a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib-dependent-issues mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 9, 2026
@mathlib-dependent-issues

mathlib-dependent-issues Bot commented Jul 9, 2026

Copy link
Copy Markdown

This PR/issue depends on:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@rmhi